T:Type, P:(TProp).
(x:T. SqStable(P(x)))  (finite-type({x:T| P(x) })  (L:T List. x:T. P(x)  (x  L))) 

latex

Definitions	t  T, x:A. B(x), x(s), (x  l), Prop, S  T, P  Q, P  Q, P  Q, P & Q, x:A. B(x), finite-type(T), SqStable(P), , l[i], ||as||, SQType(T), False, A, AB, {T}, A & B, True, T, P  Q
Lemmas	cons member, length wf1, select wf, sq stable wf, iff functionality wrt iff, finite-type-iff-list, finite-type wf, iff wf, l member wf